es:event_system{i:l}, i:Id, ds:fpf(Id; x.Type).
(x:Id. subtype_rel(es-vartype(es; i; x); fpf-cap(ds; id-deq; x; top)))
 subtype_rel(es-state(es; i); decl-state(ds)) 

latex

Definitions	Id, fpf-sub(A; a.B(a); eq; f; g), x:A. B(x), t  T, P  Q, top, id-deq, x. t(x), fpf-cap(f; eq; x; z), es-vartype(es; i; x), es-state(es; i), decl-state(ds), fpf(A; a.B(a)), event_system{i:l}
Lemmas	fpf-sub weakening, vartype-es-state-sub, event system wf, fpf wf, es-vartype wf, fpf-cap wf, Id wf, id-deq wf, top wf